es:ES, P1, Q1, P2, Q2:(E), dcd_P1:(e:EDec(P1(e))), f:({e:E| P1(e)} {e:E| Q1(e)} ),
g:({e:E| P2(e)} {e:E| Q2(e)} ).
(e:E. (P1(e))  ((P2(e))))
 (e:E. Dec(Q1(e)))
 (e:E. Dec(Q2(e)))
 Q1 = f== P1
 Q2 = g== P2
 e.(Q1(e))  (Q2(e)) = [P1? f : g]== e.(P1(e))  (P2(e)) 

latex

Definitions	x:A  B(x), f(a), left + right, P  Q, Q ==f== P, E, {x:A| B(x)} , s = t, x:A. B(x), x:AB(x), x:A. B(x), P & Q, A c B, Q = f== P, ES, t  T, Type, , Dec(P), A, P  Q, False, let x,y = A in B(x;y), t.1, e c e', b, if p:P then A(p) else B fi , [P? f : g], S  T, suptype(S; T), {T}, Void
Lemmas	conditional wf, decidable or, weak-antecedent-conditional, weak-antecedent-surjection wf, not wf, decidable wf, es-E wf, event system wf